Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    nats_active  → add_active(zeros_active)
2:    hd_active(x)  → hd(x)
3:    zeros_active  → cons(0,zeros)
4:    tl_active(x)  → tl(x)
5:    incr_active(cons(x,y))  → cons(s(x),incr(y))
6:    mark(nats)  → nats_active
7:    add_active(cons(x,y))  → incr_active(cons(x,add(y)))
8:    mark(zeros)  → zeros_active
9:    hd_active(cons(x,y))  → mark(x)
10:    mark(incr(x))  → incr_active(mark(x))
11:    tl_active(cons(x,y))  → mark(y)
12:    mark(add(x))  → add_active(mark(x))
13:    nats_active  → nats
14:    mark(hd(x))  → hd_active(mark(x))
15:    zeros_active  → zeros
16:    mark(tl(x))  → tl_active(mark(x))
17:    incr_active(x)  → incr(x)
18:    mark(0)  → 0
19:    add_active(x)  → add(x)
20:    mark(s(x))  → s(x)
21:    mark(cons(x,y))  → cons(x,y)
There are 15 dependency pairs:
22:    NATS_ACTIVE  → ADD_ACTIVE(zeros_active)
23:    NATS_ACTIVE  → ZEROS_ACTIVE
24:    MARK(nats)  → NATS_ACTIVE
25:    ADD_ACTIVE(cons(x,y))  → INCR_ACTIVE(cons(x,add(y)))
26:    MARK(zeros)  → ZEROS_ACTIVE
27:    HD_ACTIVE(cons(x,y))  → MARK(x)
28:    MARK(incr(x))  → INCR_ACTIVE(mark(x))
29:    MARK(incr(x))  → MARK(x)
30:    TL_ACTIVE(cons(x,y))  → MARK(y)
31:    MARK(add(x))  → ADD_ACTIVE(mark(x))
32:    MARK(add(x))  → MARK(x)
33:    MARK(hd(x))  → HD_ACTIVE(mark(x))
34:    MARK(hd(x))  → MARK(x)
35:    MARK(tl(x))  → TL_ACTIVE(mark(x))
36:    MARK(tl(x))  → MARK(x)
The approximated dependency graph contains one SCC: {27,29,30,32-36}. Hence the TRS is terminating.
Tyrolean Termination Tool  (9.17 seconds)   ---  May 4, 2006